nLab calculus of constructions

Idea

The Calculus of Constructions (CoC) is a type theory formal system for constructive proof in natural deduction style. This calculus goes back to Thierry Coquand and Gérard Huet

When supplemented by inductive types, it become the Calculus of Inductive Constructions (CIC). Sometimes coinductive types are included as well and one speaks of the Calculus of (co)inductive Constructions. This is what the Coq software implements.

More in detail, the Calculus of (co)Inductive Constructions is

1. a pure type system, hence

   1. a system of natural deduction with dependent types;

   2. with the natural-deduction rule for dependent product types specified;

2. with a rule for how to introduce new natural-deduction rules for arbitrary (co)inductive types.

3. and with universes:

   a cumulative hierarchy of predicative types of types

   and an impredicative type of propositions.

All of the other standard type formations are subsumed by the existence of arbitrary inductive types, notably the empty type, dependent sum types and identity types are special inductive types. Specifying these hence makes the calculus of constructions be an intensional dependent type theory.

Related concepts

• initiality conjecture

• Coq

• computational type theory

References

General

Original articles:

• Thierry Coquand, Gérard Huet, The Calculus of Constructions, INRIA Rapport 530 (1986) [inria:00076024, pdf]

• Christine Paulin-Mohring, Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) [doi:10.1007/BFb0037116]

  (adding inductive types)

Review and surveys:

• Zhaohui Luo, Computation and Reasoning – A Type Theory for Computer Science, Clarendon Press (1994) $[$ISBN:9780198538356, pdf$]$

• M. Bunder, Jonathan Seldin, Variants of the basic calculus of constructions, Journal of Applied Logic 2 2 (2004) 191-217 [doi:10.1016/j.jal.2004.02.004]

• Christine Paulin-Mohring, Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) [hal:01094195, pdf, pdf slides]

• Frade, Calculus of inductive constructions (pdf)

• Wikipedia, Calculus of constructions

A categorical semantics for CoC is discussed in

• Martin Hyland, Andy Pitts, The Theory of Constructions: Categorical Semantics and Topos-theoretic Models , Cont. Math. 92 (1989) pp.137-199. (draft)

For specifics of the implementation in Coq see

• Coq manual, Calculus of Inductive Constructions

History of inductive types

Historical references on the definition of inductive types.

Precursors

A first type theoretic formulation of general inductive definitions:

• Per Martin-Löf, Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions, Studies in Logic and the Foundations of Mathematics 63 (1971) 179-216 $[$doi:10.1016/S0049-237X(08)70847-4$]$

The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in:

• Per Martin-Löf, §1.7 and p. 94 of: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 (1975) 73-118 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

and in the modern form of inference rules in:

• Bengt Nordström, Kent Petersson, Jan M. Smith, §8.1 of: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990) $[$webpage, pdf, pdf$]$

The special case of inductive types now known as $\mathcal{W}$-types is first formulated in:

• Per Martin-Löf, pp. 171 of: Constructive Mathematics and Computer Programming, in: Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979), Studies in Logic and the Foundations of Mathematics 104 (1982) 153-175 $[$doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0$]$

• Per Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) $[$pdf, pdf$]$

Early proposals for a general formal definition of inductive types:

• Robert L. Constable, N. Paul Francis Mendler, Recursive definitions in type theory, in Logic of Programs 1985, Lecture Notes in Computer Science 193 Springer (1985) $[$doi:10.1007/3-540-15648-8_5$]$

• Paul Francis Mendler, Inductive Definition in Type Theory, Cornell (1987) $[$hdl:1813/6710$]$

• Roland Backhouse, On the Meaning and Construction of the Rules of Martin-Löf’s Theory of Types, in: Workshop on General Logic, ECS-LFCS-88-52 (1988) $[$pdf, pdf$]$

Modern definition

The modern notion of inductive types and inductive families in intensional type theory is independently due to

• Peter Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, Logical frameworks (1991) 280-306 $[$doi:10.1017/CBO9780511569807.012, pdf$]$

• Peter Dybjer, Inductive families, Formal Aspects of Computing 6 (1994) 440–465 $[$doi:10.1007/BF01211308, doi:10.1007/BF01211308, pdf$]$

and due to

• Thierry Coquand, Christine Paulin, Inductively defined types, COLOG-88 Lecture Notes in Computer Science 417, Springer (1990) 50-66 $[$doi:10.1007/3-540-52335-9_47$]$

which became the basis of the calculus of inductive constructions used in the Coq-proof assistant:

• Frank Pfenning, Christine Paulin-Mohring, Inductively defined types in the Calculus of Constructions, in: Mathematical Foundations of Programming Semantics MFPS 1989, Lecture Notes in Computer Science 442, Springer (1990) $[$doi:10.1007/BFb0040259$]$

• Christine Paulin-Mohring, Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) $[$doi:10.1007/BFb0037116$]$

reviewed in

• Zhaohui Luo, §9.2.2 in: Computation and Reasoning – A Type Theory for Computer Science, Clarendon Press (1994) $[$ISBN:9780198538356, pdf$]$

• Christine Paulin-Mohring, §2.2. in: Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) $[$hal:01094195, pdf, pdf slides$]$

with streamlined exposition in:

• Univalent Foundations Project, §5.6 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) $[$web, pdf$]$

The generalization to inductive-recursive types is due to

• Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, The Journal of Symbolic Logic 65 2 (2000) 525-549 $[$doi:10.2307/2586554, pdf$]$

• Peter Dybjer, Anton Setzer, Indexed induction-recursion, in Proof Theory in Computer Science PTCS 2001. Lecture Notes in Computer Science2183 Springer (2001) $[$doi:10.1007/3-540-45504-3_7, pdf$]$

See also:

• Peter Dybjer, Inductive and inductive-recursive definitions in type theory (link list)